%
% Copyright 2016, Data61, CSIRO (ABN 41 687 119 230)
%
% SPDX-License-Identifier: BSD-2-Clause
%

\section{Message Sequences}

This section provides a series of example message sequences for common tasks using the protocol interfaces described in \autoref{lProtocols} of this document.

\subsection{Server Registration}

\autoref{f:servreg} illustrates the protocol a server uses to register itself under a name.

\begin{figure}[htb]
\begin{center}
\begin{msc}
msc {
    hscale = "1.5";

    R [ label ="Name Server"],
    S [ label = "Data Server"];
    
    S box S [ label = "create badged endpoint capability dataserv\_anon\_C"];
 
    S => R [ label = "nameserv\_session\_C.register(\"server\_name\", dataserv\_anon\_C)"];
    R box R [ label = "handle request, register under given name"];
    R >> S [ label = "ErrorCode"];
}
\end{msc}
\end{center}
\caption{Server registration protocol}
\label{f:servreg}
\end{figure}

\subsection{Establish a Session to a Server}


\autoref{f:estab} illustrates that to interact with a server one must establish a session with the server through the server's anonymous endpoint capability. An established session with a server is represented by a \obj{session} capability with the server knowing the security subject of the client and optionally death notifications set up so that the server is informed when the client exits and at this time can modify its bookkeeping accordingly.

\begin{figure}[htb]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";

        R [ label ="Process Server"],
        F [ label = "File Server"],
        C [ label = "Client"],
        N [ label ="Name Server"];

        R:>C [ label = "procserv\_liveness\_C"];
        C box C [label = "loop until path fully resolved:"];
        C=>N [ label = "nameserv\_session\_C.resolve\_segment(\"dataserver\")"];
        N>>C [ label = "(ErrorCode, dataserv\_anon\_C)"];
        C=>F [ label = "dataserv\_anon\_C.connect(procserv\_liveness\_C)"];
        F box F [label = "handle request, create client"];
        F=>R [ label = "procserv\_session\_C.watch\_client(procserv\_liveness\_C)"];
        R box R [ label = "set up death notify"];
        R>>F [ label = "(ErrorCode, death\_id, principle\_id)"];
        F box F [ label = "create session capability for new client"];
        F>>C [ label = "(dataserv\_session\_C)"];
      }
    \end{msc}
  \end{center}
  \caption{Example message sequence for finding and establishing a connection with a server}
  \label{f:estab}
\end{figure}

Note that the (optional) argument principle\_id is intended to be used for authentication assuming an ACL-like security model in the file system.

\pagebreak

\subsection{Opening and Closing a Dataspace}

\autoref{f:openclose} shows how a client opens a dataspace which could subsequently be used for mapping in a window. This example also shows how a dataspace is closed.

\begin{figure}[htb]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";

        D [ label = "Data Server"],
        C [ label = "Client"];

        C=>D [ label = "dataserv\_session\_C.open(name, flags, mode, size)"];
        D box D [label = "handle request, create dataspace"];
        D>>C [ label = "(ErrorCode, dataserv\_dataspace\_C)"];
        C box C [label="read/write/share/use dataspace"];
        C=>D [label = "dataserv\_session\_C.close(dataserv\_session\_C)"];
        D>>C [label = "ErrorCode" ];
      }
    \end{msc}
  \end{center}
  \caption{Sample protocol for opening and closing a dataspace}
  \label{f:openclose}
\end{figure}


\subsection{Map a Dataspace into a Window}

\autoref{f:opendata} shows mapping an open dataspace into a given memory window. The initialisation sets up the components for sample fault delegation in the system.  Note that the process server is acting as the memory manager. The paging could instead be implemented through a separate memory manager process.

\begin{figure}[htb]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";

        R [ label = "Process Server"],
        P [ label = "Data Server"],
        C [ label = "Client"];

        C abox P [ label = "Create a dataspace" ];
        C=>R [ label = "procserv\_session\_C.create\_mem\_window(base, size, perms, flags)"];
        R>>C [ label = "(ErrorCode, procserv\_window\_C)"];
        C=>P [ label = "dataserv\_session\_C.datamap(dataserv\_dataspace\_C, procserv\_window\_C, offset)"];
        P box P [label = "validate request"];
        P=>R [ label = "procserv\_session\_C.register\_as\_pager(procserv\_window\_C, dataserv\_notify\_C)"];
        R box R [ label = "bookkeep pager information"];
        R>>P [ label = "(ErrorCode, window\_id)"];
        P>>C [ label = "ErrorCode"];
      }
    \end{msc}
  \end{center}
  \caption{Sample protocol for mapping a dataspace into a given window}
  \label{f:opendata}
\end{figure}

\subsection{Page Fault}

\autoref{f:pagefault} shows the page fault resolution protocol in the case of an external dataspace server backing a window in the client's address space. In \refOS, the \seLf microkernel sends the page fault notification to an endpoint capability pretending to be the faulting process.

\begin{figure}[h]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";
        
        K [ label ="Kernel"],
        P [ label ="Process Server"],
        C [ label = "Client"],
        D [ label = "Data Server"];
       
        C box C [label = "VM fault into mapped dataspace"];
        K->P [label = "Page fault notification"];
        P box P [label = "transform fault into window\_id, offset"];
        P->D [ label = "dataserv\_event\_C.pagefault\_notify(window\_id,offset,op)"];
        D=>P [ label = "procserv\_session\_C.window\_map(window\_cap, window\_offset, src\_addr)"];
        P box P [ label = "handle request and find frame"];
        P:>C [ label = "map\_frame(frame)"];
        P>>D [ label = "ErrorCode"];
        P:>C [ label = "Resume execution"];
      }
    \end{msc}
  \end{center}
  \caption{Page fault protocol}
  \label{f:pagefault}
\end{figure}

\clearpage
\subsection{Death Notification}
\autoref{f:deathnotify} illustrates an example death notification protocol. Note that it is assumed that the client is active and has already established a connection with the data server (see \autoref{f:estab}) and that the data server has subsequently set up death notification.

\begin{figure}[h]
\begin{center}
\begin{msc}
  msc {
    hscale = "1.5";

    C [ label = "Client"],
    P [ label = "Process Server"],
    D [ label = "Data Server"];
    
    C box C [ label = "Exits program" ];
    C => P [ label = "procserv\_session\_C.exit(status)" ];
    P box P [ label = "Delete client process" ];
    P >> D [ label = "dataserv\_event\_C.death\_notify(death\_id)" ];
    D box D [ label = "Delete client session bookkeeping" ];
  }
\end{msc}
\end{center}
\caption{Example death notification protocol}
\label{f:deathnotify}
\end{figure}

\subsection{Dataspace Sharing}

\autoref{f:sharedata} is an example of how to set up a shared dataspace. Note that it is assumed that the share is not revocable and that sharing is with an entity that is trusted. Therefore, given two clients, at least one of the clients must trust the other client. Mutual distrust is not supported yet because capability transfer to an untrusted entity requires more than a direct call.

In this example, the shared dataspace is implemented by the process server (acting as the memory manager) and is shared with a server. This is typical for a shared memory communication buffer.

\begin{figure}[h]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";

        R [ label ="Process Server"],
        C [ label = "Client"],
        D [ label = "Server"];
        
        C=>R [ label = "procserv\_session\_C.open(\"anon\", flags, mode, size)"];
        R>>C [ label = "(ErrorCode, procserv\_dataspace\_C)"];
        --- [ label = "Client maps the dataspace" ];
        C=>R [ label = "procserv\_process\_C.create\_mem\_window(base, size, perm, flags)"];
        R>>C [ label = "(ErrorCode, procserv\_window\_C)"];
        C=>R [ label = "procserv\_session\_C.datamap(procserv\_dataspace\_C, procserv\_window\_C, offset)"];
        R>>C [ label = "ErrorCode"];
        --- [ label = "Share to dataspace capability with server"];
        C=>D [ label = "serv\_session\_C.datashare(procserv\_dataspace\_C)"];
        D=>R [ label = "procserv\_process\_C.Create\_mem\_window(base, flags, mode, size)"];
        R>>D [ label = "(ErrorCode, procserv\_window2\_C)"];
        D=>R [ label = "procserv\_session\_C.datamap(procserv\_dataspace\_C, procserv\_window2\_C, offset)"];
        R>>D [ label = "ErrorCode"];
        D>>C [ label = "ErrorCode"];
        D abox C [ label = "Communicate using shared dataspace" ];
      }
    \end{msc}
  \end{center}
  \caption{Sample protocol for sharing an anonymous dataspace}
  \label{f:sharedata}
\end{figure}

\clearpage

\autoref{f:sharedatathird} provides another example of dataspace sharing. In this example, the dataspace is implemented by an external data server instead of by the process server. A third party is involved in this case. This is a more general example of \autoref{f:sharedata}.

\begin{figure}[h]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";

        R [ label ="Process Server"],
        D [ label = "Data Server"],
        CA [ label = "Client A"],
        CB [ label = "Client B"];
        
        CA=>D [ label = "dataserv\_session\_C.open(\"filename\", flags, mode, size)"];
        D>>CA [ label = "(ErrorCode, dataserv\_dataspace\_C)"];

        --- [ label = "Client A maps the dataspace" ];
        CA=>R [ label = "procserv\_session\_C.create\_mem\_window(base, size, perm, flags)"];
        R>>CA [ label = "(ErrorCode, procserv\_window\_C)"];
        CA=>D [ label = "dataserv\_session\_C.datamap(dataserv\_dataspace\_C, procserv\_window\_C, offset)"];
        D=>R [ label = "procserv\_session\_C.register\_as\_pager(procserv\_window\_C, dataserv\_notify\_C)"];
        R box R [ label = "Bookkeep pager information"];
        R>>D [ label = "(ErrorCode, window\_id)"];
        D>>CA [ label = "ErrorCode"];

        --- [ label = "Now share the dataspace with client B"];
        CA=>CB [ label = "clientB\_session\_C.datashare(dataserv\_dataspace\_C)"];

        --- [ label = "Client B also maps the dataspace"];
        CB=>R [ label = "procserv\_session\_C.create\_mem\_window(base, size, perm, flags)"];
        R>>CB [ label = "(ErrorCode, procserv\_window2\_C)"];
        CB=>D [ label = "dataserv\_session\_C.datamap(dataserv\_dataspace\_C, procserv\_window2\_C, offset)"];
        D=>R [ label = "procserv\_session\_C.register\_as\_pager(procserv\_window2\_C, dataserv\_notify\_C)"];
        R box R [ label = "Bookkeep pager information"];
        R>>D [ label = "(ErrorCode, window\_id)"];
        D>>CB [ label = "ErrorCode"];

        --- [ label = "Both clients have dataspace mapped"];
        CA abox CB [ label = "Communicate using shared dataspace." ];
      }
    \end{msc}
  \end{center}
  \caption{Sample protocol for sharing a dataspace provided by a dataspace server}
  \label{f:sharedatathird}
\end{figure}

\clearpage
\subsection{Content Initialise a Dataspace with Another Dataspace}

\autoref{f:initdata} shows creating a dataspace and setting the dataspace so that it is initialised with the contents of another dataspace. This example initialises a RAM dataspace (with the process server acting as its data server as per \refOS's implementation) with the contents of an executable file from another dataspace.

\begin{figure}[htb]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";

        P [ label ="Process Server"],
        D [ label = "Data Server"],
        C [ label = "Client"];

        --- [ label = "Open the dataspace to be initialised"];
        C=>P [ label = "proc\_session\_C.open(\"anon\", flags, mode, size)"];
        P>>C [ label = "(ErrorCode, procserv\_dataspace\_C)"];

        --- [ label = "Open the data space to initialise with"];
        C=>D [ label = "dataserv\_session\_C.open(\"binary\", flags, mode, size)"];
        D>>C [ label = "(ErrorCode, dataserv\_dataspace\_C)"];

        --- [ label = "Initialise procserv dataspace with dataserv dataspace"];
        C=>D [ label = "dataserv\_session\_C.init\_data(procserv\_dataspace\_C, dataserv\_dataspace\_C, src\_offset)"];
        D box D [label = "Validate request and bookkeep dataspace relationship"];
        D=>P [ label = "procserv\_process\_C.have\_data(procserv\_dataspace\_C, dataserv\_notify\_C)"];
        P box P [ label = "Bookkeep pager information"];
        P>>D [ label = "(ErrorCode, data\_id)"];
        D>>C [ label = "ErrorCode"];

        --- [ label = "Now have dataspace initialised by external data server"];
        C=>P [ label = "procserv\_process\_C.create\_mem\_window(base, size, perm, flags)"];
        P>>C [ label = "(ErrorCode, procserv\_window\_C)"];
        C=>P [ label = "procserv\_session\_C.datamap(procserv\_dataspace\_C, procserv\_window\_C, offset)"];
        P>>C [ label = "ErrorCode"];

        C box C [ label = "Read from content-initialised mapped dataspace"];
      }
    \end{msc}
  \end{center}
  \caption{Sample protocol for creating a dataspace initialised with the contents of another dataspace}
  \label{f:initdata}
\end{figure}

\clearpage
\subsection{Content Initialised Page Fault}

\autoref{f:initfault} illustrates the page fault resolution protocol in the case of an external dataspace server providing the initial data for the dataspace. Note the similarity with \autoref{f:pagefault}. The difference between the two protocols is that in the content initialised page fault protocol the content in the frame provided by the data server is not used by the client; instead the content of the frame is copied to the receiving dataserver's dataspace. In contrast, the regular page fault protocol directly maps the physical frame into the client's address space.

\begin{figure}[htb]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";
        
        K [ label = "Kernel"],
        P [ label ="Process Server"],
        C [ label = "Client"],
        D [ label = "Data Server"];
        
        C box C [label = "VM fault into mapped dataspace"];
        K->P [label = "Page fault notification"];
        P box P [label = "transform fault into window\_id, offset"];
        P->D [ label = "dataserv\_event\_C.initfault\_notify(data\_id, offset)"];
        D=>P [ label = "procserv\_session\_C.provide\_data(data\_id, src\_addr, offset)"];
        P box P [ label = "validate and find frame and copy data"];
        P:>C [ label = "map\_frame(frame)"];
        P>>D [ label = "ErrorCode"];
        P:>C [ label = "Resume execution"];
      }
    \end{msc}
  \end{center}
  \caption{Data content initialisation fault protocol}
  \label{f:initfault}
\end{figure}

\subsection{ELF loading}

\autoref{f:elfloading} shows the elf loading protocol for bootstrapping a user process.

\begin{figure}[htb]
  \begin{center}
    \begin{msc}
      msc {
        hscale = "1.5";
        
        P [ label ="Process Server"],
        D [ label = "Data Server"],
        C [ label = "Client"];
        
        --- [ label = "User process starts at elf loading code in its own address space"];
        P abox C [ label = "Datamap ELF header file contents"];
        C box C [ label = "read ELF header"];

        --- [ label = "For each section (code/data):"];
        
        C => P [ label = "procserv\_session\_C.create\_mem\_window(base, size, perm, flags)"];
        P >> C [ label = "(ErrorCode, procserv\_window\_C)"];
        P abox C [ label = "Content initialise dataspace with code/data section content"];
        C => P [ label = "procserv\_session\_C.datamap(procserv\_dataspace\_C, procserv\_window\_C, offset)"];
        P >> C [ label = "ErrorCode"];

        P abox C [ label = "Create anonymous dataspace for zeroed section"];
        C => P [ label = "procserv\_session\_C.create\_mem\_window(base, size, perm, flags)"];
        P >> C [ label = "(ErrorCode, procserv\_window2\_C)"];
        P abox C [ label = "Datamap zeroed section into window"];

        --- [ label = "After all sections have been mapped:"];
        C box C [ label = "jump to program entry point"];
        C box C [ label = "set up userland environment"];
      }
    \end{msc}
  \end{center}
  \caption{Elf loading protocol}
  \label{f:elfloading}
\end{figure}

\clearpage
\section{Data Structures}

This section provides an approximate representation of a number of data structures that \refOS employs. These data structures are only meant to be a guideline and are presented in the C language. These data structures aim to be the minimal information such a structure should store and intend to convey an idea of what these objects represent. Implementations may need to add extra members and references to these data structures to allow for internal bookkeeping.

\subsection {Memory Window}

A memory window should bookkeep its state, which vspace it belongs to, where and how long the memory segment is and the state of the memory window's contents. A memory window may be unmapped or mapped to a dataspace, and that dataspace may or may not be content initialised. In \refOS, the process server is the anonymous memory dataserver, so in \refOS the memory window data structure has extra bookkeeping information for the internal anonymous dataspace mapping state. Also, \refOS separates the memory window's size and offset into multiple windows.

\begin{verbatim}
struct w_window {
    vspace_t *vspace;
    vaddr_t offset;
    vaddr_t size;
    uint32_t permissions;
    bool cacheable;
    cspacepath_t capability;
    pager_t pager;
};
\end{verbatim}

\subsection {Process Control Block}

A process control block data structure should bookkeep its address space (capability space and virtual memory space), its threads and the clients it is watching. \refOS also contains parameter buffers, notification ring buffers, the process operating system capabilities bitmask, the parent process's ID, the debug name and a number of other bookkeeping parameters.

\begin{verbatim}
struct proc_pcb {
    struct vs_vspace vspace;
    proc_tcb threads[];
    struct proc_watch_list clientWatchList;
};
\end{verbatim}

\subsection {Anonymous Dataspace}

An anonymous dataspace data structure needs to bookkeep its capability, the list of frame pages it is representing and its content initialisation data. The content initialisation bitmask records which pages in the dataspace have been initialised and which still need to be initialised. Initialisation happens lazily, on the first VM fault, so a waiting list of clients that are VM fault blocked waiting for content to be initialised needs to be recorded.

\begin{verbatim}
struct ram_dspace {
    cspacepath_t capability;
    vka_object_t *pages;
    uint32_t npages;
    cspacepath_t contentInitEP;
    uint32_t *contentInitBitmask;
    cvector_t contentInitWaitingList;
};
\end{verbatim}

\subsection {Archived File Server Dataspace}

An archived file server dataspace assumes that there is a char* storing the file data somewhere in the process server's address space. In \refOS, this comes from a cpio format archive linked into the process's ELF sections.

\begin{verbatim}
struct fs_dataspace {
    seL4_CPtr dataspaceCap;
    seL4_Word permissions;
    char *fileData;
    size_t fileDataSize;
    content_init_info_t contentInitInfo;
};
\end{verbatim}

\subsection {Userland Dataspace Mapping}

A userland dataspace mapping data strucure must bookkeep its window, dataspace and session and the virtual address and size of the memory window segment.

\begin{verbatim}
typedef struct data_mapping {
    seL4_CPtr session;
    seL4_CPtr dataspace;
    seL4_CPtr window;
    char* vaddr;
    int windowSize;
    int dspaceSize;
} data_mapping_t;
\end{verbatim}
